$\forall$$T$:Type, ${\it op}$:($T$$\rightarrow$$T$$\rightarrow$$T$), ${\it id}$:$T$, ${\it inv}$:($T$$\rightarrow$$T$).
\\[0ex]Assoc($T$;${\it op}$) $\Rightarrow$ Ident($T$;${\it op}$;${\it id}$) $\Rightarrow$ Inverse($T$;${\it op}$;${\it id}$;${\it inv}$) $\Rightarrow$ (mk\_igrp($T$;${\it op}$;${\it id}$;${\it inv}$) $\in$ IGroup)